i || a
== Trans(i):k:Kndkindtype(i;k)es_state(es;i)es_state(es;i)||a
== & Send(i):k:Kndkindtype(i;k)state@i(Msg List)||a
== & Choose(i):b:Idstate@i(?kindtype(i;locl(b)))||a 

latex

---

clarification:

es-atom(es;i;a)
== free-from-atom{1}(k:Kndes-kindtype(es;i;k)es_state(es;i)es_state(es;i);es-trans(es;i);a)
== & free-from-atom{1}(k:Kndes-kindtype(es;i;k)es-state(es;i)
== (es-Msg(es) List);es-send(es;i);a)
== & free-from-atom{1}(b:Ides-state(es;i)
== & (es-kindtype(es;i;locl(b)) + Unit);es-choose(es;i);a) 

latex

Definitions	es_state(es;i), Trans(i), P & Q, Knd, type List, Msg, Send(i), Id, , x:AB(x), state@i, left + right, kindtype(i;k), locl(a), Unit, Choose(i)
FDL editor aliases	es-atom